T:Type, l1,l2,l3:(T List).
iseg(T; l1; append(l2; l3))
 (iseg(T; l1; l2)  (l:T List. ((0 < ||l||)  (l1 = append(l2; l))  iseg(T; l; l3)))) 

latex

Definitions	t  T, iseg(T; l1; l2), P  Q, x:A. B(x), P  Q, P  Q, x:A. B(x), append(as; bs), prop{i:l}, ||as||, P  Q, P  Q, A c B, ge(i; j), guard(T), False, b, hd(l), A, A  B, tl(l)
Lemmas	tl wf, ge wf, hd wf, iseg append, or functionality wrt iff, cons iseg, iseg nil, length cons, non neg length, nil iseg, length wf1, append wf, iseg wf